$\forall$${\it es}$:ES, ${\it Fail}$:AbsInterface(Top), $A$:Type, $X$:AbsInterface($A$), $e$:E.
\\[0ex]($\uparrow$($e$ $\in_{b}$ alive($X$))) $\Rightarrow$ (alive($X$)($e$) = $X$($e$) $\in$ $A$)